Skip to content

Conversation

strub
Copy link
Member

@strub strub commented Jan 13, 2025

The import mechanism is currently brittle, buggy, interact wrongly with the cloning mechanism. Moreover, some declarations duplicate it by reimplementing an ad-hoc, "non-import" mechanism.

@strub strub self-assigned this Jan 13, 2025
@strub strub changed the title Remove "non-import" flags from axioms Rework import mechanism Jan 20, 2025
@strub strub marked this pull request as ready for review January 20, 2025 10:00
@strub
Copy link
Member Author

strub commented Jan 20, 2025

Removed all ad-hoc mechanisms, clean-up general one, correct interaction with cloning.

Yet has to be extended => future PR.

@strub strub force-pushed the hidden-theory-items branch from 19e8269 to fdd7813 Compare January 20, 2025 10:03
@strub strub requested review from fdupress and bgregoir January 20, 2025 10:03
@strub strub force-pushed the hidden-theory-items branch from fdd7813 to fa18670 Compare January 20, 2025 12:33
Copy link
Member

@fdupress fdupress left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems to retain functionality for all proofs we wish to (and can) preserve—including some not yet in external CI. But I can't vouch for internals — @bgregoir will need to review those.

@strub strub force-pushed the hidden-theory-items branch 2 times, most recently from 7066af3 to 6dfe829 Compare February 6, 2025 17:26
@strub strub force-pushed the hidden-theory-items branch 2 times, most recently from 92a15e6 to 67dc10a Compare August 22, 2025 20:14
The import mechanism is currently brittle, buggy, interact wrongly
with the cloning mechanism. Moreover, some declarations duplicate it
by reimplementing an ad-hoc, "non-import" mechanism. This commit fixes
this issues.
@strub strub force-pushed the hidden-theory-items branch from 67dc10a to 3673b82 Compare August 23, 2025 09:43
@strub strub removed the request for review from bgregoir August 23, 2025 09:46
@strub strub merged commit b60d136 into main Aug 23, 2025
15 checks passed
@strub strub deleted the hidden-theory-items branch August 23, 2025 12:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants